T:Type, R, Q:(TT).
(x, y:T. (R(x,y))  (Q(x,y)))
 (n:, x, y:T. (rel_exp(T;R;n)(x,y))  (rel_exp(T;Q;n)(x,y))) 

latex

Definitions	Void, a < b, n - m, n+m, -n, #$n, A  B, A, False, i  j , {x:A| B(x)} , , Type, P  Q, P  Q, f(a), rel_exp(T;R;n), x:AB(x), x:A. B(x), t  T, , left + right, Unit, x:A  B(x), , , b, x.A(x), P & Q, P  Q, s = t, (i = j), b, x:A. B(x), x f y, A c B
Lemmas	and functionality wrt iff, rel exp wf, le wf, assert wf, not wf, bnot wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, nat wf, nat properties, ge wf